a, b:Knd. Dec(a = b) 

latex

Definitions	x. t(x), P  Q, P & Q, P  Q, P  Q, a = b, t  T, Prop, Knd, Dec(P), b, x:A. B(x)
Lemmas	decidable assert, assert wf, eq knd wf, decidable wf, Knd wf, assert-eq-knd, decidable functionality, all functionality wrt iff